\begin{tabbing}
crossed{-}pair\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it ff}$; ${\it is\_req}$; ${\it is\_ack}$; ${\it sndr}$; ${\it rcvr}$; $r$; $a$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=${\it ff}$.S(${\it sndr}$,${\it rcvr}$,$r$)\+
\\[0ex]\& ${\it is\_req}$($r$)
\\[0ex]\& ${\it ff}$.S(${\it rcvr}$,${\it sndr}$,$a$)
\\[0ex]\& ${\it is\_ack}$($a$)
\\[0ex]\& ($\exists$\=${\it r'}$:\{$e$:es{-}E(${\it es}$)$\mid$ ${\it ff}$.R(${\it rcvr}$,$e$)\} \+
\\[0ex]$\exists$\=${\it a'}$:\{$e$:es{-}E(${\it es}$)$\mid$ ${\it ff}$.R(${\it sndr}$,$e$)\} \+
\\[0ex](${\it ff}$.Sender(${\it rcvr}$,${\it r'}$) = $r$ $\in$ es{-}E(${\it es}$)
\\[0ex]\& ${\it ff}$.Sender(${\it sndr}$,${\it a'}$) = $a$ $\in$ es{-}E(${\it es}$)
\\[0ex]\& es{-}causl(${\it es}$; $r$; ${\it a'}$)
\\[0ex]\& es{-}causl(${\it es}$; $a$; ${\it r'}$)))
\-\-\-
\end{tabbing}